x, y:Atom1. (x =a1 y)  (x = y) 

latex

Definitions	eq_atom$n(x;y), , t  T, P  Q, P  Q, P & Q, P  Q, x:A. B(x), False, A, P  Q, Dec(P)
Lemmas	btrue wf, eqtt to assert, assert of bnot, bfalse wf, eqff to assert, decidable atom equal 1, eq atom wf1, assert wf